g:OCMon, a, b, c:|g|. (a  b)  (b < c)  (a < c) 

latex

Up	groups 1
Definitions of Statement	Mon, AbMon, gset, OMon, OCMon, goset, a  b, a < b
Definitions	x,y. t(x;y), , x f y, OMon, t  T, x:A. B(x), t.2, t.1, , gset, POSet{i}, Mon, x(s1,s2), P & Q, AbMon, LOSet, goset, a  b, |p|, OCMon, a < b, a  b
Lemmas	ocmon wf, loset wf, grp le wf, assert wf, grp car wf, linorder wf, oset of ocmon wf, set lt transitivity 1